(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun T_1t0_72450_457 () (_ BitVec 1))
(declare-fun T_32t5_72455_456 () (_ BitVec 32))
(declare-fun R_OF_15_453 () (_ BitVec 1))
(declare-fun R_SF_14_447 () (_ BitVec 1))
(declare-fun R_ZF_13_444 () (_ BitVec 1))
(declare-fun T_6319_72459_421 () (_ BitVec 32))
(declare-fun T_32t6_72467_415 () (_ BitVec 32))
(declare-fun T_64t2_72463_414 () (_ BitVec 64))
(declare-fun T_1t0_72503_303 () (_ BitVec 1))
(declare-fun T_32t5_72508_302 () (_ BitVec 32))
(declare-fun R_OF_15_300 () (_ BitVec 1))
(declare-fun R_SF_14_294 () (_ BitVec 1))
(declare-fun T_6316_72512_268 () (_ BitVec 32))
(declare-fun T_32t6_72520_262 () (_ BitVec 32))
(declare-fun T_64t2_72516_261 () (_ BitVec 64))
(declare-fun temp_253 () (_ BitVec 64))
(declare-fun T_32t1_72540_230 () (_ BitVec 32))
(declare-fun T_32t1_72545_221 () (_ BitVec 32))
(declare-fun T_32t0_72548_185 () (_ BitVec 32))
(declare-fun T_32t2_72557_176 () (_ BitVec 32))
(declare-fun mem_35_681 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun mem_35_678 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun mem_35_675 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun mem_35_673 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun t_672 () (_ BitVec 1))
(declare-fun t_671 () (_ BitVec 1))
(declare-fun t_670 () (_ BitVec 1))
(declare-fun t_669 () (_ BitVec 1))
(declare-fun t_668 () (_ BitVec 1))
(declare-fun t_667 () (_ BitVec 1))
(declare-fun t_666 () (_ BitVec 1))
(declare-fun t_665 () (_ BitVec 1))
(declare-fun t_664 () (_ BitVec 1))
(declare-fun t_663 () (_ BitVec 1))
(declare-fun t_662 () (_ BitVec 1))
(declare-fun t_661 () (_ BitVec 1))
(declare-fun t_660 () (_ BitVec 1))
(declare-fun t_659 () (_ BitVec 1))
(declare-fun t_658 () (_ BitVec 1))
(declare-fun t_657 () (_ BitVec 1))
(declare-fun t_656 () (_ BitVec 1))
(declare-fun t_655 () (_ BitVec 1))
(declare-fun R_EBX_6_85 () (_ BitVec 32))
(declare-fun t_654 () (_ BitVec 1))
(declare-fun t_653 () (_ BitVec 1))
(declare-fun t_652 () (_ BitVec 1))
(declare-fun R_EAX_5_82 () (_ BitVec 32))
(declare-fun t_651 () (_ BitVec 1))
(declare-fun t_650 () (_ BitVec 1))
(declare-fun R_ESI_2_80 () (_ BitVec 32))
(declare-fun t_649 () (_ BitVec 1))
(declare-fun t_648 () (_ BitVec 1))
(declare-fun t_647 () (_ BitVec 1))
(declare-fun t_646 () (_ BitVec 1))
(declare-fun t_645 () (_ BitVec 1))
(declare-fun t_644 () (_ BitVec 1))
(declare-fun t_643 () (_ BitVec 1))
(declare-fun t_642 () (_ BitVec 1))
(declare-fun t_641 () (_ BitVec 1))
(declare-fun t_640 () (_ BitVec 1))
(declare-fun t_639 () (_ BitVec 1))
(declare-fun t_638 () (_ BitVec 1))
(declare-fun R_EDX_8_64 () (_ BitVec 32))
(declare-fun R_EBP_0_60 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert (let ((?v_0 (bvnot (_ bv0 1))) (?v_1 (bvor (bvand (bvshl (bvsmod (_ bv0 64) temp_253) (_ bv32 64)) (_ bv0 64)) (bvand (bvsdiv (_ bv0 64) temp_253) (_ bv0 64))))) (= (_ bv1 1) (bvand (bvand (ite (= t_638 (_ bv0 1)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_639 ?v_0) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_640 (_ bv0 1)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_641 ?v_0) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_642 T_1t0_72450_457) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_643 (bvnot T_1t0_72450_457)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_644 T_1t0_72503_303) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_645 (bvor t_642 t_643)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_646 (ite (= T_1t0_72450_457 ((_ extract 0 0) T_32t5_72455_456)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_647 (ite (= T_32t5_72455_456 (concat (_ bv0 31) (bvor (bvxor R_SF_14_447 R_OF_15_453) R_ZF_13_444))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_648 (ite (= R_OF_15_453 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor T_32t1_72540_230 T_32t6_72467_415) (bvxor T_32t1_72540_230 T_6319_72459_421)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_649 (ite (= R_SF_14_447 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr T_6319_72459_421 (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_650 (ite (= R_ZF_13_444 (ite (= T_6319_72459_421 (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_651 (ite (= T_6319_72459_421 (bvsub T_32t1_72540_230 T_32t6_72467_415)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_652 (ite (= T_32t6_72467_415 ((_ extract 31 0) T_64t2_72463_414)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_653 (ite (= T_64t2_72463_414 ?v_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_654 (bvor t_640 t_641)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_655 (bvnot T_1t0_72503_303)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_656 (bvor t_644 (bvand t_655 (bvand t_654 (bvand t_653 (bvand t_652 (bvand t_651 (bvand t_650 (bvand t_649 (bvand t_648 (bvand t_647 (bvand t_646 t_645)))))))))))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_657 (ite (= T_1t0_72503_303 ((_ extract 0 0) T_32t5_72508_302)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_658 (ite (= T_32t5_72508_302 (concat (_ bv0 31) (bvxor R_SF_14_294 R_OF_15_300))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_659 (ite (= R_OF_15_300 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor T_32t1_72540_230 T_32t6_72520_262) (bvxor T_32t1_72540_230 T_6316_72512_268)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_660 (ite (= R_SF_14_294 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr T_6316_72512_268 (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_661 (ite (= T_6316_72512_268 (bvsub T_32t1_72540_230 T_32t6_72520_262)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_662 (ite (= T_32t6_72520_262 ((_ extract 31 0) T_64t2_72516_261)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_663 (ite (= T_64t2_72516_261 ?v_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_664 (ite (= temp_253 ((_ sign_extend 32) R_EDX_8_64)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_665 (bvor t_638 t_639)) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_666 (ite (= T_32t1_72540_230 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_673 (bvadd R_EAX_5_82 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_673 (bvadd R_EAX_5_82 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_673 (bvadd R_EAX_5_82 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_673 (bvadd R_EAX_5_82 (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_667 (ite (= mem_35_673 (store (store (store (store mem_35_675 (bvadd T_32t0_72548_185 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_85 (_ bv24 32)))) (bvadd T_32t0_72548_185 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_85 (_ bv16 32)))) (bvadd T_32t0_72548_185 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_85 (_ bv8 32)))) (bvadd T_32t0_72548_185 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_85))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_668 (ite (= mem_35_675 (store (store (store (store mem_35_678 (bvadd T_32t1_72545_221 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_ESI_2_80 (_ bv24 32)))) (bvadd T_32t1_72545_221 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_ESI_2_80 (_ bv16 32)))) (bvadd T_32t1_72545_221 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_ESI_2_80 (_ bv8 32)))) (bvadd T_32t1_72545_221 (_ bv0 32)) ((_ extract 7 0) R_ESI_2_80))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_669 (ite (= T_32t1_72545_221 (bvadd T_32t0_72548_185 (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_670 (ite (= T_32t0_72548_185 (bvsub T_32t2_72557_176 (_ bv8 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= t_671 (ite (= mem_35_678 (store (store (store (store mem_35_681 (bvadd T_32t2_72557_176 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv24 32)))) (bvadd T_32t2_72557_176 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv16 32)))) (bvadd T_32t2_72557_176 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv8 32)))) (bvadd T_32t2_72557_176 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_60))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= t_672 (ite (= T_32t2_72557_176 (bvsub R_ESP_1_58 (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))))))))) (bvand ?v_0 (bvand (bvand t_672 (bvand t_671 (bvand t_670 (bvand t_669 (bvand t_668 (bvand t_667 (bvand t_666 (bvand t_665 (bvand t_664 (bvand t_663 (bvand t_662 (bvand t_661 (bvand t_660 (bvand t_659 (bvand t_658 (bvand t_657 t_656)))))))))))))))) (_ bv1 1)))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
